\begin{tabbing}
$k$\=(v:$B$) sends\+
\\[0ex]$f$($x$:$A$,v) on
\\[0ex]$l$ tagged with ${\it tg}$:$T$
\\[0ex]provided $c$($x$,v)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=((vartype(source($l$);$x$) $\subseteq$r $A$)\+
\\[0ex]\& ($\forall$$e$:E. (loc($e$) = source($l$)) $\Rightarrow$ (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r $B$))
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = source($l$))
\\[0ex]$\Rightarrow$ (kind($e$) = $k$)
\\[0ex]$\Rightarrow$ \=((\=($\uparrow$($c$(($x$ when $e$),val($e$))))\+\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex]((kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]c$\wedge$ \=(sender(${\it e'}$) = $e$\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex](kind(${\it e''}$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (sender(${\it e''}$) = $e$) $\Rightarrow$ (${\it e''}$ = ${\it e'}$))
\-\\[0ex]\& val(${\it e'}$) = $f$(($x$ when $e$),val($e$))))))
\-\-\-\\[0ex]\& (\=($\neg$($\uparrow$($c$(($x$ when $e$),val($e$)))))\+
\\[0ex]$\Rightarrow$ ($\neg$($\exists$${\it e'}$:E. ((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (sender(${\it e'}$) = $e$)))))))
\-\-\-\-
\end{tabbing}